Nuprl Lemma : es-kindtype-w-valtype
0,22
postcript
pdf
i
:Id,
w
:World,
p
:FairFifo,
k
:Knd,
v
:Top. kindtype(
i
;
k
) ~ valtype(
i
;doact(
k
;
v
))
latex
Definitions
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
isrcv(
k
)
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
kind(
a
)
,
es-V(
es
)
,
es-M(
es
)
,
valtype(
i
;
a
)
,
doact(
k
;
v
)
,
kindtype(
i
;
k
)
,
ES(
the_w
)
,
Id
,
t
T
,
World
,
x
:
A
.
B
(
x
)
,
FairFifo
,
Top
Lemmas
top
wf
,
Knd
wf
,
fair-fifo
wf
,
world
wf
,
Id
wf
origin
i:Id, w:World, p:FairFifo, k:Knd, v:Top. kindtype(i;k) ~ valtype(i;doact(k;v)) i:Id, w:World, p:FairFifo, k:Knd, v:Top. kindtype(i;k) ~ valtype(i;doact(k;v)) 
B(x)
Tx:A. B(x)